The present disclosure is directed to Boolean Satisfiability (SAT) instances and more particularly to using reconfigurable computing devices to solve SAT instances.
Boolean Satisfiability (SAT) is the problem of finding values for a set of Boolean variables that makes a given Boolean formula (evaluate to) TRUE. SAT is an NP-complete problem. If no assignment of the Boolean variables makes the Boolean formula TRUE, then the formula is called unsatisfiable. The formula is typically presented in a conjunctive normal form (CNF). That is, the formula is presented as the conjunction (logical AND operation) of a set of disjunctions (logical OR operations) of one or more Boolean literals. The literals consist of variables or their logical negation. This is a general form since arbitrary Boolean functions can be reduced to a CNF.
Typically, in solving SAT, software running on general-purpose computers is utilized, which is necessarily based on the Turing machine paradigm of computation. SAT solvers come in two varieties depending on their behavior when the given Boolean formula is unsatisfiable. Complete methods are guaranteed to terminate in all cases and provide a proof that the given formula is unsatisfiable. Incomplete methods only terminate when a satisfying assignment of the variables is found; if the algorithm proceeds beyond a user-definable threshold number of steps, it is assumed that the formula is unsatisfiable, but there is no proof that it truly is unsatisfiable.
Reconfigurable computing devices such as field-programmable gate arrays (FPGAs) can also be used to accelerate solving SAT instances. These approaches, however, are hardware implementations of classical algorithms and thus reducible to the Turing paradigm.